Nuprl Definition : grp_blt
13,42
postcript
pdf
a
<
b
==
a
<
b
latex
clarification:
a
<
g
b
==
a
<
(
g
oset)
b
latex
Up
groups
1
Wellformedness Lemmas
grp
blt
wf
Definitions
a
<
b
,
g
oset
origin
b == a < b
g b == a <(g
oset) b b == a < b
g b == a <(goset) b boset